(0) Obligation:

Clauses:

goal :- ','(np(S1, S2, S), verb(S2, S3, S)).
parse(S0, Meaning) :- ','(np(S0, S1, Meaning), verb(S1, [], Meaning)).
parse(S0, Meaning) :- ','(np(S0, S1, Meaning), ','(verb(S1, S2, Meaning), =(S2, []))).
np(Si, So, S) :- ','(det(Si, St, T), ','(noun(St, So, N), comb(T, N, S))).
comb(a, -(N, s), s(s, N, V)).
comb(the, -(N, P), s(P, N, V)).
det(.(a, S), S, a).
det(.(the, S), S, the).
noun(.(book, S), S, -(book, s)).
noun(.(books, S), S, -(book, p)).
noun(.(box, S), S, -(box, s)).
noun(.(boxes, S), S, -(box, p)).
verb(.(falls, So), So, s(s, N, fall)).
verb(.(fall, So), So, s(p, N, fall)).
verb(.(flies, So), So, s(s, N, fly)).
verb(.(fly, So), So, s(p, N, fly)).

Query: parse(g,a)

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

(2) Obligation:

Clauses:

parseA(.(a, .(book, .(falls, []))), s(s, book, fall)).
parseA(.(a, .(book, .(flies, []))), s(s, book, fly)).
parseA(.(a, .(box, .(falls, []))), s(s, box, fall)).
parseA(.(a, .(box, .(flies, []))), s(s, box, fly)).
parseA(.(the, .(book, .(falls, []))), s(s, book, fall)).
parseA(.(the, .(book, .(flies, []))), s(s, book, fly)).
parseA(.(the, .(books, .(fall, []))), s(p, book, fall)).
parseA(.(the, .(books, .(fly, []))), s(p, book, fly)).
parseA(.(the, .(box, .(falls, []))), s(s, box, fall)).
parseA(.(the, .(box, .(flies, []))), s(s, box, fly)).
parseA(.(the, .(boxes, .(fall, []))), s(p, box, fall)).
parseA(.(the, .(boxes, .(fly, []))), s(p, box, fly)).
parseA(.(a, .(book, .(falls, []))), s(s, book, fall)).
parseA(.(a, .(book, .(flies, []))), s(s, book, fly)).
parseA(.(a, .(box, .(falls, []))), s(s, box, fall)).
parseA(.(a, .(box, .(flies, []))), s(s, box, fly)).
parseA(.(the, .(book, .(falls, []))), s(s, book, fall)).
parseA(.(the, .(book, .(flies, []))), s(s, book, fly)).
parseA(.(the, .(books, .(fall, []))), s(p, book, fall)).
parseA(.(the, .(books, .(fly, []))), s(p, book, fly)).
parseA(.(the, .(box, .(falls, []))), s(s, box, fall)).
parseA(.(the, .(box, .(flies, []))), s(s, box, fly)).
parseA(.(the, .(boxes, .(fall, []))), s(p, box, fall)).
parseA(.(the, .(boxes, .(fly, []))), s(p, box, fly)).

Query: parseA(g,a)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

parseA_in_ga(.(a, .(book, .(falls, []))), s(s, book, fall)) → parseA_out_ga(.(a, .(book, .(falls, []))), s(s, book, fall))
parseA_in_ga(.(a, .(book, .(flies, []))), s(s, book, fly)) → parseA_out_ga(.(a, .(book, .(flies, []))), s(s, book, fly))
parseA_in_ga(.(a, .(box, .(falls, []))), s(s, box, fall)) → parseA_out_ga(.(a, .(box, .(falls, []))), s(s, box, fall))
parseA_in_ga(.(a, .(box, .(flies, []))), s(s, box, fly)) → parseA_out_ga(.(a, .(box, .(flies, []))), s(s, box, fly))
parseA_in_ga(.(the, .(book, .(falls, []))), s(s, book, fall)) → parseA_out_ga(.(the, .(book, .(falls, []))), s(s, book, fall))
parseA_in_ga(.(the, .(book, .(flies, []))), s(s, book, fly)) → parseA_out_ga(.(the, .(book, .(flies, []))), s(s, book, fly))
parseA_in_ga(.(the, .(books, .(fall, []))), s(p, book, fall)) → parseA_out_ga(.(the, .(books, .(fall, []))), s(p, book, fall))
parseA_in_ga(.(the, .(books, .(fly, []))), s(p, book, fly)) → parseA_out_ga(.(the, .(books, .(fly, []))), s(p, book, fly))
parseA_in_ga(.(the, .(box, .(falls, []))), s(s, box, fall)) → parseA_out_ga(.(the, .(box, .(falls, []))), s(s, box, fall))
parseA_in_ga(.(the, .(box, .(flies, []))), s(s, box, fly)) → parseA_out_ga(.(the, .(box, .(flies, []))), s(s, box, fly))
parseA_in_ga(.(the, .(boxes, .(fall, []))), s(p, box, fall)) → parseA_out_ga(.(the, .(boxes, .(fall, []))), s(p, box, fall))
parseA_in_ga(.(the, .(boxes, .(fly, []))), s(p, box, fly)) → parseA_out_ga(.(the, .(boxes, .(fly, []))), s(p, box, fly))

The argument filtering Pi contains the following mapping:
parseA_in_ga(x1, x2)  =  parseA_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
a  =  a
book  =  book
falls  =  falls
[]  =  []
parseA_out_ga(x1, x2)  =  parseA_out_ga(x2)
flies  =  flies
box  =  box
the  =  the
books  =  books
fall  =  fall
fly  =  fly
boxes  =  boxes

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

parseA_in_ga(.(a, .(book, .(falls, []))), s(s, book, fall)) → parseA_out_ga(.(a, .(book, .(falls, []))), s(s, book, fall))
parseA_in_ga(.(a, .(book, .(flies, []))), s(s, book, fly)) → parseA_out_ga(.(a, .(book, .(flies, []))), s(s, book, fly))
parseA_in_ga(.(a, .(box, .(falls, []))), s(s, box, fall)) → parseA_out_ga(.(a, .(box, .(falls, []))), s(s, box, fall))
parseA_in_ga(.(a, .(box, .(flies, []))), s(s, box, fly)) → parseA_out_ga(.(a, .(box, .(flies, []))), s(s, box, fly))
parseA_in_ga(.(the, .(book, .(falls, []))), s(s, book, fall)) → parseA_out_ga(.(the, .(book, .(falls, []))), s(s, book, fall))
parseA_in_ga(.(the, .(book, .(flies, []))), s(s, book, fly)) → parseA_out_ga(.(the, .(book, .(flies, []))), s(s, book, fly))
parseA_in_ga(.(the, .(books, .(fall, []))), s(p, book, fall)) → parseA_out_ga(.(the, .(books, .(fall, []))), s(p, book, fall))
parseA_in_ga(.(the, .(books, .(fly, []))), s(p, book, fly)) → parseA_out_ga(.(the, .(books, .(fly, []))), s(p, book, fly))
parseA_in_ga(.(the, .(box, .(falls, []))), s(s, box, fall)) → parseA_out_ga(.(the, .(box, .(falls, []))), s(s, box, fall))
parseA_in_ga(.(the, .(box, .(flies, []))), s(s, box, fly)) → parseA_out_ga(.(the, .(box, .(flies, []))), s(s, box, fly))
parseA_in_ga(.(the, .(boxes, .(fall, []))), s(p, box, fall)) → parseA_out_ga(.(the, .(boxes, .(fall, []))), s(p, box, fall))
parseA_in_ga(.(the, .(boxes, .(fly, []))), s(p, box, fly)) → parseA_out_ga(.(the, .(boxes, .(fly, []))), s(p, box, fly))

The argument filtering Pi contains the following mapping:
parseA_in_ga(x1, x2)  =  parseA_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
a  =  a
book  =  book
falls  =  falls
[]  =  []
parseA_out_ga(x1, x2)  =  parseA_out_ga(x2)
flies  =  flies
box  =  box
the  =  the
books  =  books
fall  =  fall
fly  =  fly
boxes  =  boxes

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
P is empty.
The TRS R consists of the following rules:

parseA_in_ga(.(a, .(book, .(falls, []))), s(s, book, fall)) → parseA_out_ga(.(a, .(book, .(falls, []))), s(s, book, fall))
parseA_in_ga(.(a, .(book, .(flies, []))), s(s, book, fly)) → parseA_out_ga(.(a, .(book, .(flies, []))), s(s, book, fly))
parseA_in_ga(.(a, .(box, .(falls, []))), s(s, box, fall)) → parseA_out_ga(.(a, .(box, .(falls, []))), s(s, box, fall))
parseA_in_ga(.(a, .(box, .(flies, []))), s(s, box, fly)) → parseA_out_ga(.(a, .(box, .(flies, []))), s(s, box, fly))
parseA_in_ga(.(the, .(book, .(falls, []))), s(s, book, fall)) → parseA_out_ga(.(the, .(book, .(falls, []))), s(s, book, fall))
parseA_in_ga(.(the, .(book, .(flies, []))), s(s, book, fly)) → parseA_out_ga(.(the, .(book, .(flies, []))), s(s, book, fly))
parseA_in_ga(.(the, .(books, .(fall, []))), s(p, book, fall)) → parseA_out_ga(.(the, .(books, .(fall, []))), s(p, book, fall))
parseA_in_ga(.(the, .(books, .(fly, []))), s(p, book, fly)) → parseA_out_ga(.(the, .(books, .(fly, []))), s(p, book, fly))
parseA_in_ga(.(the, .(box, .(falls, []))), s(s, box, fall)) → parseA_out_ga(.(the, .(box, .(falls, []))), s(s, box, fall))
parseA_in_ga(.(the, .(box, .(flies, []))), s(s, box, fly)) → parseA_out_ga(.(the, .(box, .(flies, []))), s(s, box, fly))
parseA_in_ga(.(the, .(boxes, .(fall, []))), s(p, box, fall)) → parseA_out_ga(.(the, .(boxes, .(fall, []))), s(p, box, fall))
parseA_in_ga(.(the, .(boxes, .(fly, []))), s(p, box, fly)) → parseA_out_ga(.(the, .(boxes, .(fly, []))), s(p, box, fly))

The argument filtering Pi contains the following mapping:
parseA_in_ga(x1, x2)  =  parseA_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
a  =  a
book  =  book
falls  =  falls
[]  =  []
parseA_out_ga(x1, x2)  =  parseA_out_ga(x2)
flies  =  flies
box  =  box
the  =  the
books  =  books
fall  =  fall
fly  =  fly
boxes  =  boxes

We have to consider all (P,R,Pi)-chains

(6) Obligation:

Pi DP problem:
P is empty.
The TRS R consists of the following rules:

parseA_in_ga(.(a, .(book, .(falls, []))), s(s, book, fall)) → parseA_out_ga(.(a, .(book, .(falls, []))), s(s, book, fall))
parseA_in_ga(.(a, .(book, .(flies, []))), s(s, book, fly)) → parseA_out_ga(.(a, .(book, .(flies, []))), s(s, book, fly))
parseA_in_ga(.(a, .(box, .(falls, []))), s(s, box, fall)) → parseA_out_ga(.(a, .(box, .(falls, []))), s(s, box, fall))
parseA_in_ga(.(a, .(box, .(flies, []))), s(s, box, fly)) → parseA_out_ga(.(a, .(box, .(flies, []))), s(s, box, fly))
parseA_in_ga(.(the, .(book, .(falls, []))), s(s, book, fall)) → parseA_out_ga(.(the, .(book, .(falls, []))), s(s, book, fall))
parseA_in_ga(.(the, .(book, .(flies, []))), s(s, book, fly)) → parseA_out_ga(.(the, .(book, .(flies, []))), s(s, book, fly))
parseA_in_ga(.(the, .(books, .(fall, []))), s(p, book, fall)) → parseA_out_ga(.(the, .(books, .(fall, []))), s(p, book, fall))
parseA_in_ga(.(the, .(books, .(fly, []))), s(p, book, fly)) → parseA_out_ga(.(the, .(books, .(fly, []))), s(p, book, fly))
parseA_in_ga(.(the, .(box, .(falls, []))), s(s, box, fall)) → parseA_out_ga(.(the, .(box, .(falls, []))), s(s, box, fall))
parseA_in_ga(.(the, .(box, .(flies, []))), s(s, box, fly)) → parseA_out_ga(.(the, .(box, .(flies, []))), s(s, box, fly))
parseA_in_ga(.(the, .(boxes, .(fall, []))), s(p, box, fall)) → parseA_out_ga(.(the, .(boxes, .(fall, []))), s(p, box, fall))
parseA_in_ga(.(the, .(boxes, .(fly, []))), s(p, box, fly)) → parseA_out_ga(.(the, .(boxes, .(fly, []))), s(p, box, fly))

The argument filtering Pi contains the following mapping:
parseA_in_ga(x1, x2)  =  parseA_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
a  =  a
book  =  book
falls  =  falls
[]  =  []
parseA_out_ga(x1, x2)  =  parseA_out_ga(x2)
flies  =  flies
box  =  box
the  =  the
books  =  books
fall  =  fall
fly  =  fly
boxes  =  boxes

We have to consider all (P,R,Pi)-chains

(7) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,R,Pi) chain.

(8) YES